YES 1.551
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule List
| ((isPrefixOf :: Eq a => [[a]] -> [[a]] -> Bool) :: Eq a => [[a]] -> [[a]] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] _ | = | True |
isPrefixOf | _ [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((isPrefixOf :: Eq a => [[a]] -> [[a]] -> Bool) :: Eq a => [[a]] -> [[a]] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (isPrefixOf :: Eq a => [[a]] -> [[a]] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy2000), Succ(xy4001000)) → new_primPlusNat(xy2000, xy4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy2000), Succ(xy4001000)) → new_primPlusNat(xy2000, xy4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy300100), Succ(xy400100)) → new_primMulNat(xy300100, Succ(xy400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy300100), Succ(xy400100)) → new_primMulNat(xy300100, Succ(xy400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy30000), Succ(xy40000)) → new_primEqNat(xy30000, xy40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy30000), Succ(xy40000)) → new_primEqNat(xy30000, xy40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(app(ty_@2, bcg), bch)), hg), bbb)) → new_esEs2(xy3000, xy4000, bcg, bch)
new_esEs1(Right(xy3000), Right(xy4000), df, app(ty_Maybe, dg)) → new_esEs0(xy3000, xy4000, dg)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(app(ty_@2, bad), bae))) → new_esEs2(xy3002, xy4002, bad, bae)
new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(ty_[], eb))) → new_esEs(xy3000, xy4000, eb)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(ty_Maybe, bba)), bbb)) → new_esEs0(xy3001, xy4001, bba)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(ty_Maybe, bba), bbb) → new_esEs0(xy3001, xy4001, bba)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(ty_[], gh)), ge)) → new_esEs(xy3000, xy4000, gh)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(app(app(ty_@3, hc), hd), he)), ge)) → new_esEs3(xy3000, xy4000, hc, hd, he)
new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(app(ty_@2, ec), ed))) → new_esEs2(xy3000, xy4000, ec, ed)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(ty_Maybe, hh)) → new_esEs0(xy3002, xy4002, hh)
new_esEs0(Just(xy3000), Just(xy4000), app(ty_Maybe, bb)) → new_esEs0(xy3000, xy4000, bb)
new_esEs0(Just(xy3000), Just(xy4000), app(ty_[], be)) → new_esEs(xy3000, xy4000, be)
new_esEs1(Left(xy3000), Left(xy4000), app(app(ty_Either, ce), cf), cd) → new_esEs1(xy3000, xy4000, ce, cf)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(ty_Maybe, bcc)), hg), bbb)) → new_esEs0(xy3000, xy4000, bcc)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(app(app(ty_@3, ga), gb), gc)) → new_esEs3(xy3001, xy4001, ga, gb, gc)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(ty_[], bbe), bbb) → new_esEs(xy3001, xy4001, bbe)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(ty_[], ff))) → new_esEs(xy3001, xy4001, ff)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bcd), bce), hg, bbb) → new_esEs1(xy3000, xy4000, bcd, bce)
new_esEs1(Left(xy3000), Left(xy4000), app(app(ty_@2, da), db), cd) → new_esEs2(xy3000, xy4000, da, db)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(app(app(ty_@3, bda), bdb), bdc)), hg), bbb)) → new_esEs3(xy3000, xy4000, bda, bdb, bdc)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_Maybe, gd), ge) → new_esEs0(xy3000, xy4000, gd)
new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(ty_[], cg)), cd)) → new_esEs(xy3000, xy4000, cg)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(app(ty_Either, bbc), bbd), bbb) → new_esEs1(xy3001, xy4001, bbc, bbd)
new_esEs0(Just(xy3000), Just(xy4000), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xy3000, xy4000, bh, ca, cb)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bcg), bch), hg, bbb) → new_esEs2(xy3000, xy4000, bcg, bch)
new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(app(app(ty_@3, dc), dd), de)), cd)) → new_esEs3(xy3000, xy4000, dc, dd, de)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(app(ty_Either, fc), fd))) → new_esEs1(xy3001, xy4001, fc, fd)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(ty_Maybe, hh))) → new_esEs0(xy3002, xy4002, hh)
new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(app(ty_@2, da), db)), cd)) → new_esEs2(xy3000, xy4000, da, db)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(app(ty_Either, gf), gg)), ge)) → new_esEs1(xy3000, xy4000, gf, gg)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bcc), hg, bbb) → new_esEs0(xy3000, xy4000, bcc)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(app(app(ty_@3, bbh), bca), bcb)), bbb)) → new_esEs3(xy3001, xy4001, bbh, bca, bcb)
new_esEs1(Right(xy3000), Right(xy4000), df, app(ty_[], eb)) → new_esEs(xy3000, xy4000, eb)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_Either, gf), gg), ge) → new_esEs1(xy3000, xy4000, gf, gg)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(ty_[], bac))) → new_esEs(xy3002, xy4002, bac)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(app(ty_@3, hc), hd), he), ge) → new_esEs3(xy3000, xy4000, hc, hd, he)
new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(ty_Maybe, dg))) → new_esEs0(xy3000, xy4000, dg)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(ty_[], bbe)), bbb)) → new_esEs(xy3001, xy4001, bbe)
new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(app(ty_Either, ce), cf)), cd)) → new_esEs1(xy3000, xy4000, ce, cf)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(app(ty_@2, bbf), bbg)), bbb)) → new_esEs2(xy3001, xy4001, bbf, bbg)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(app(ty_@2, fg), fh))) → new_esEs2(xy3001, xy4001, fg, fh)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(app(app(ty_@3, baf), bag), bah)) → new_esEs3(xy3002, xy4002, baf, bag, bah)
new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(ty_Maybe, cc)), cd)) → new_esEs0(xy3000, xy4000, cc)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(ty_[], bcf)), hg), bbb)) → new_esEs(xy3000, xy4000, bcf)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(ty_[], bac)) → new_esEs(xy3002, xy4002, bac)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(app(ty_@2, fg), fh)) → new_esEs2(xy3001, xy4001, fg, fh)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(app(ty_Either, bcd), bce)), hg), bbb)) → new_esEs1(xy3000, xy4000, bcd, bce)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(ty_Maybe, fb)) → new_esEs0(xy3001, xy4001, fb)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_[], bcf), hg, bbb) → new_esEs(xy3000, xy4000, bcf)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_@2, ha), hb), ge) → new_esEs2(xy3000, xy4000, ha, hb)
new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(ty_[], be))) → new_esEs(xy3000, xy4000, be)
new_esEs1(Right(xy3000), Right(xy4000), df, app(app(ty_Either, dh), ea)) → new_esEs1(xy3000, xy4000, dh, ea)
new_esEs1(Left(xy3000), Left(xy4000), app(ty_Maybe, cc), cd) → new_esEs0(xy3000, xy4000, cc)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(app(app(ty_@3, baf), bag), bah))) → new_esEs3(xy3002, xy4002, baf, bag, bah)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(app(ty_Either, fc), fd)) → new_esEs1(xy3001, xy4001, fc, fd)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(app(app(ty_@3, bbh), bca), bcb), bbb) → new_esEs3(xy3001, xy4001, bbh, bca, bcb)
new_esEs0(Just(xy3000), Just(xy4000), app(app(ty_@2, bf), bg)) → new_esEs2(xy3000, xy4000, bf, bg)
new_esEs(:(xy300, xy301), :(xy400, xy401), ba) → new_esEs(xy301, xy401, ba)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(ty_[], ff)) → new_esEs(xy3001, xy4001, ff)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(app(ty_@2, bad), bae)) → new_esEs2(xy3002, xy4002, bad, bae)
new_esEs0(Just(xy3000), Just(xy4000), app(app(ty_Either, bc), bd)) → new_esEs1(xy3000, xy4000, bc, bd)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(app(ty_Either, baa), bab))) → new_esEs1(xy3002, xy4002, baa, bab)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(app(ty_@2, bbf), bbg), bbb) → new_esEs2(xy3001, xy4001, bbf, bbg)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(ty_Maybe, gd)), ge)) → new_esEs0(xy3000, xy4000, gd)
new_esEs1(Right(xy3000), Right(xy4000), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xy3000, xy4000, ee, ef, eg)
new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(app(ty_@2, bf), bg))) → new_esEs2(xy3000, xy4000, bf, bg)
new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(ty_Maybe, bb))) → new_esEs0(xy3000, xy4000, bb)
new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(app(app(ty_@3, bh), ca), cb))) → new_esEs3(xy3000, xy4000, bh, ca, cb)
new_esEs1(Right(xy3000), Right(xy4000), df, app(app(ty_@2, ec), ed)) → new_esEs2(xy3000, xy4000, ec, ed)
new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xy3000, xy4000, ee, ef, eg)
new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(app(ty_Either, bc), bd))) → new_esEs1(xy3000, xy4000, bc, bd)
new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_[], gh), ge) → new_esEs(xy3000, xy4000, gh)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(app(ty_@2, ha), hb)), ge)) → new_esEs2(xy3000, xy4000, ha, hb)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(app(ty_Either, baa), bab)) → new_esEs1(xy3002, xy4002, baa, bab)
new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(app(ty_Either, dh), ea))) → new_esEs1(xy3000, xy4000, dh, ea)
new_esEs1(Left(xy3000), Left(xy4000), app(ty_[], cg), cd) → new_esEs(xy3000, xy4000, cg)
new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(app(ty_Either, bbc), bbd)), bbb)) → new_esEs1(xy3001, xy4001, bbc, bbd)
new_esEs1(Left(xy3000), Left(xy4000), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xy3000, xy4000, dc, dd, de)
new_esEs(:(xy300, xy301), :(xy400, xy401), app(ty_[], eh)) → new_esEs(xy300, xy400, eh)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(ty_Maybe, fb))) → new_esEs0(xy3001, xy4001, fb)
new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bda), bdb), bdc), hg, bbb) → new_esEs3(xy3000, xy4000, bda, bdb, bdc)
new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(app(app(ty_@3, ga), gb), gc))) → new_esEs3(xy3001, xy4001, ga, gb, gc)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs0(Just(xy3000), Just(xy4000), app(ty_[], be)) → new_esEs(xy3000, xy4000, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xy3000), Just(xy4000), app(app(ty_Either, bc), bd)) → new_esEs1(xy3000, xy4000, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xy3000), Just(xy4000), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xy3000, xy4000, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xy3000), Just(xy4000), app(ty_Maybe, bb)) → new_esEs0(xy3000, xy4000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xy3000), Just(xy4000), app(app(ty_@2, bf), bg)) → new_esEs2(xy3000, xy4000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(ty_[], ff)) → new_esEs(xy3001, xy4001, ff)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_[], gh), ge) → new_esEs(xy3000, xy4000, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_Either, gf), gg), ge) → new_esEs1(xy3000, xy4000, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(app(ty_Either, fc), fd)) → new_esEs1(xy3001, xy4001, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(app(app(ty_@3, ga), gb), gc)) → new_esEs3(xy3001, xy4001, ga, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(app(ty_@3, hc), hd), he), ge) → new_esEs3(xy3000, xy4000, hc, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_Maybe, gd), ge) → new_esEs0(xy3000, xy4000, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(ty_Maybe, fb)) → new_esEs0(xy3001, xy4001, fb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), fa, app(app(ty_@2, fg), fh)) → new_esEs2(xy3001, xy4001, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_@2, ha), hb), ge) → new_esEs2(xy3000, xy4000, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(ty_[], eb))) → new_esEs(xy3000, xy4000, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(ty_[], gh)), ge)) → new_esEs(xy3000, xy4000, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(ty_[], ff))) → new_esEs(xy3001, xy4001, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(ty_[], cg)), cd)) → new_esEs(xy3000, xy4000, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(ty_[], bac))) → new_esEs(xy3002, xy4002, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(ty_[], bbe)), bbb)) → new_esEs(xy3001, xy4001, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(ty_[], bcf)), hg), bbb)) → new_esEs(xy3000, xy4000, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(ty_[], be))) → new_esEs(xy3000, xy4000, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy300, xy301), :(xy400, xy401), ba) → new_esEs(xy301, xy401, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xy300, xy301), :(xy400, xy401), app(ty_[], eh)) → new_esEs(xy300, xy400, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(ty_[], bbe), bbb) → new_esEs(xy3001, xy4001, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(ty_[], bac)) → new_esEs(xy3002, xy4002, bac)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_[], bcf), hg, bbb) → new_esEs(xy3000, xy4000, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(xy3000), Right(xy4000), df, app(ty_[], eb)) → new_esEs(xy3000, xy4000, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xy3000), Left(xy4000), app(ty_[], cg), cd) → new_esEs(xy3000, xy4000, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(app(ty_Either, fc), fd))) → new_esEs1(xy3001, xy4001, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(app(ty_Either, gf), gg)), ge)) → new_esEs1(xy3000, xy4000, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(app(ty_Either, ce), cf)), cd)) → new_esEs1(xy3000, xy4000, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(app(ty_Either, bcd), bce)), hg), bbb)) → new_esEs1(xy3000, xy4000, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(app(ty_Either, baa), bab))) → new_esEs1(xy3002, xy4002, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(app(ty_Either, bc), bd))) → new_esEs1(xy3000, xy4000, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(app(ty_Either, dh), ea))) → new_esEs1(xy3000, xy4000, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(app(ty_Either, bbc), bbd)), bbb)) → new_esEs1(xy3001, xy4001, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bcd), bce), hg, bbb) → new_esEs1(xy3000, xy4000, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(app(ty_Either, bbc), bbd), bbb) → new_esEs1(xy3001, xy4001, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(app(ty_Either, baa), bab)) → new_esEs1(xy3002, xy4002, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(Left(xy3000), Left(xy4000), app(app(ty_Either, ce), cf), cd) → new_esEs1(xy3000, xy4000, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xy3000), Right(xy4000), df, app(app(ty_Either, dh), ea)) → new_esEs1(xy3000, xy4000, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(app(app(ty_@3, hc), hd), he)), ge)) → new_esEs3(xy3000, xy4000, hc, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(app(app(ty_@3, bda), bdb), bdc)), hg), bbb)) → new_esEs3(xy3000, xy4000, bda, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(app(app(ty_@3, dc), dd), de)), cd)) → new_esEs3(xy3000, xy4000, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(app(app(ty_@3, bbh), bca), bcb)), bbb)) → new_esEs3(xy3001, xy4001, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(app(app(ty_@3, baf), bag), bah))) → new_esEs3(xy3002, xy4002, baf, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(app(app(ty_@3, bh), ca), cb))) → new_esEs3(xy3000, xy4000, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xy3000, xy4000, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(app(app(ty_@3, ga), gb), gc))) → new_esEs3(xy3001, xy4001, ga, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(ty_Maybe, bba)), bbb)) → new_esEs0(xy3001, xy4001, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(ty_Maybe, bcc)), hg), bbb)) → new_esEs0(xy3000, xy4000, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(ty_Maybe, hh))) → new_esEs0(xy3002, xy4002, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(ty_Maybe, dg))) → new_esEs0(xy3000, xy4000, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(ty_Maybe, cc)), cd)) → new_esEs0(xy3000, xy4000, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(ty_Maybe, gd)), ge)) → new_esEs0(xy3000, xy4000, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(ty_Maybe, bb))) → new_esEs0(xy3000, xy4000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(ty_Maybe, fb))) → new_esEs0(xy3001, xy4001, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, app(app(ty_@2, bcg), bch)), hg), bbb)) → new_esEs2(xy3000, xy4000, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), hg), app(app(ty_@2, bad), bae))) → new_esEs2(xy3002, xy4002, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Right(xy3000), xy301), :(Right(xy4000), xy401), app(app(ty_Either, df), app(app(ty_@2, ec), ed))) → new_esEs2(xy3000, xy4000, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Left(xy3000), xy301), :(Left(xy4000), xy401), app(app(ty_Either, app(app(ty_@2, da), db)), cd)) → new_esEs2(xy3000, xy4000, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xy3000, xy3001, xy3002), xy301), :(@3(xy4000, xy4001, xy4002), xy401), app(app(app(ty_@3, hf), app(app(ty_@2, bbf), bbg)), bbb)) → new_esEs2(xy3001, xy4001, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, fa), app(app(ty_@2, fg), fh))) → new_esEs2(xy3001, xy4001, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Just(xy3000), xy301), :(Just(xy4000), xy401), app(ty_Maybe, app(app(ty_@2, bf), bg))) → new_esEs2(xy3000, xy4000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@2(xy3000, xy3001), xy301), :(@2(xy4000, xy4001), xy401), app(app(ty_@2, app(app(ty_@2, ha), hb)), ge)) → new_esEs2(xy3000, xy4000, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(app(app(ty_@3, baf), bag), bah)) → new_esEs3(xy3002, xy4002, baf, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(app(app(ty_@3, bbh), bca), bcb), bbb) → new_esEs3(xy3001, xy4001, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bda), bdb), bdc), hg, bbb) → new_esEs3(xy3000, xy4000, bda, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Right(xy3000), Right(xy4000), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xy3000, xy4000, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(Left(xy3000), Left(xy4000), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xy3000, xy4000, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(ty_Maybe, bba), bbb) → new_esEs0(xy3001, xy4001, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(ty_Maybe, hh)) → new_esEs0(xy3002, xy4002, hh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bcc), hg, bbb) → new_esEs0(xy3000, xy4000, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bcg), bch), hg, bbb) → new_esEs2(xy3000, xy4000, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, hg, app(app(ty_@2, bad), bae)) → new_esEs2(xy3002, xy4002, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), hf, app(app(ty_@2, bbf), bbg), bbb) → new_esEs2(xy3001, xy4001, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Right(xy3000), Right(xy4000), df, app(ty_Maybe, dg)) → new_esEs0(xy3000, xy4000, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xy3000), Left(xy4000), app(ty_Maybe, cc), cd) → new_esEs0(xy3000, xy4000, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(xy3000), Left(xy4000), app(app(ty_@2, da), db), cd) → new_esEs2(xy3000, xy4000, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xy3000), Right(xy4000), df, app(app(ty_@2, ec), ed)) → new_esEs2(xy3000, xy4000, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba) → new_isPrefixOf(xy31, xy41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba) → new_isPrefixOf(xy31, xy41, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3